Страх и ненависть в Групоиде

У нас было 8 систем типов, 5 конструкторов, теория категорий, категория
функторов, два сопряженных функтора и их эквивалентность, предел функтора,
категория сетодиов вместе со своей высшей категорией их отображений. А также
для зависимой теории — категория зависимых сетоидов, слайс категория сеторидов,
категория фукнторрв между ними, два сопряжения описывающе Пи и Сигма,
и, наконец, утверждение о комутативсности треугольника в LCCC.
Не то чтобы это был необходимый запас для поездки, но если начал собирать категории,
становится трудно остановится. Единственное, что вызывало у меня опасение — это элиминатор индукции
induction_on. Ничто в мире не бывает более беспомощным, безотвественным и
порочным, чем человек, который не может написать на CoC-овском лямбда
ассемблере зависимый элиминиатор индукции объекта натуральных чисел. Я знал что
рано или поздно мы напишем его и перейдем на эту дрянь окончательно.